f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), a) → F(x, g(a))
F(g(x), g(y)) → H(g(y), x, g(y))
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), a) → F(x, g(a))
F(g(x), g(y)) → H(g(y), x, g(y))
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(g(x), a) → F(x, g(a))
Used ordering: Polynomial interpretation [25,35]:
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), g(y)) → H(g(y), x, g(y))
The value of delta used in the strict ordering is 1.
POL(a) = 4
POL(g(x1)) = 0
POL(h(x1, x2, x3)) = (4)x_3
POL(f(x1, x2)) = 0
POL(F(x1, x2)) = (1/4)x_2
POL(H(x1, x2, x3)) = x_3
f(a, g(y)) → g(g(y))
h(g(x), y, z) → f(y, h(x, y, z))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(a, y, z) → z
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
H(g(x), y, z) → F(y, h(x, y, z))
H(g(x), y, z) → H(x, y, z)
F(g(x), g(y)) → H(g(y), x, g(y))
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(g(x), y, z) → F(y, h(x, y, z))
F(g(x), g(y)) → H(g(y), x, g(y))
Used ordering: Polynomial interpretation [25,35]:
H(g(x), y, z) → H(x, y, z)
The value of delta used in the strict ordering is 4.
POL(a) = 0
POL(g(x1)) = 4 + x_1
POL(h(x1, x2, x3)) = 0
POL(f(x1, x2)) = 0
POL(F(x1, x2)) = (2)x_1
POL(H(x1, x2, x3)) = 4 + (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
H(g(x), y, z) → H(x, y, z)
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(g(x), y, z) → H(x, y, z)
The value of delta used in the strict ordering is 8.
POL(g(x1)) = 4 + (4)x_1
POL(H(x1, x2, x3)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f(a, g(y)) → g(g(y))
f(g(x), a) → f(x, g(a))
f(g(x), g(y)) → h(g(y), x, g(y))
h(g(x), y, z) → f(y, h(x, y, z))
h(a, y, z) → z